Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

+(0, y) → y
+(s(x), y) → s(+(x, y))
++(nil, ys) → ys
++(:(x, xs), ys) → :(x, ++(xs, ys))
sum(:(x, nil)) → :(x, nil)
sum(:(x, :(y, xs))) → sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) → sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(-(x, y), s(y)))
length(nil) → 0
length(:(x, xs)) → s(length(xs))
hd(:(x, xs)) → x
avg(xs) → quot(hd(sum(xs)), length(xs))

Q is empty.


↳ QTRS
  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

+(0, y) → y
+(s(x), y) → s(+(x, y))
++(nil, ys) → ys
++(:(x, xs), ys) → :(x, ++(xs, ys))
sum(:(x, nil)) → :(x, nil)
sum(:(x, :(y, xs))) → sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) → sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(-(x, y), s(y)))
length(nil) → 0
length(:(x, xs)) → s(length(xs))
hd(:(x, xs)) → x
avg(xs) → quot(hd(sum(xs)), length(xs))

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

SUM(++(xs, :(x, :(y, ys)))) → ++1(xs, sum(:(x, :(y, ys))))
AVG(xs) → HD(sum(xs))
QUOT(s(x), s(y)) → -1(x, y)
LENGTH(:(x, xs)) → LENGTH(xs)
-1(s(x), s(y)) → -1(x, y)
+1(s(x), y) → +1(x, y)
AVG(xs) → QUOT(hd(sum(xs)), length(xs))
AVG(xs) → SUM(xs)
++1(:(x, xs), ys) → ++1(xs, ys)
AVG(xs) → LENGTH(xs)
SUM(:(x, :(y, xs))) → +1(x, y)
SUM(:(x, :(y, xs))) → SUM(:(+(x, y), xs))
QUOT(s(x), s(y)) → QUOT(-(x, y), s(y))
SUM(++(xs, :(x, :(y, ys)))) → SUM(:(x, :(y, ys)))
SUM(++(xs, :(x, :(y, ys)))) → SUM(++(xs, sum(:(x, :(y, ys)))))

The TRS R consists of the following rules:

+(0, y) → y
+(s(x), y) → s(+(x, y))
++(nil, ys) → ys
++(:(x, xs), ys) → :(x, ++(xs, ys))
sum(:(x, nil)) → :(x, nil)
sum(:(x, :(y, xs))) → sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) → sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(-(x, y), s(y)))
length(nil) → 0
length(:(x, xs)) → s(length(xs))
hd(:(x, xs)) → x
avg(xs) → quot(hd(sum(xs)), length(xs))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ EdgeDeletionProof

Q DP problem:
The TRS P consists of the following rules:

SUM(++(xs, :(x, :(y, ys)))) → ++1(xs, sum(:(x, :(y, ys))))
AVG(xs) → HD(sum(xs))
QUOT(s(x), s(y)) → -1(x, y)
LENGTH(:(x, xs)) → LENGTH(xs)
-1(s(x), s(y)) → -1(x, y)
+1(s(x), y) → +1(x, y)
AVG(xs) → QUOT(hd(sum(xs)), length(xs))
AVG(xs) → SUM(xs)
++1(:(x, xs), ys) → ++1(xs, ys)
AVG(xs) → LENGTH(xs)
SUM(:(x, :(y, xs))) → +1(x, y)
SUM(:(x, :(y, xs))) → SUM(:(+(x, y), xs))
QUOT(s(x), s(y)) → QUOT(-(x, y), s(y))
SUM(++(xs, :(x, :(y, ys)))) → SUM(:(x, :(y, ys)))
SUM(++(xs, :(x, :(y, ys)))) → SUM(++(xs, sum(:(x, :(y, ys)))))

The TRS R consists of the following rules:

+(0, y) → y
+(s(x), y) → s(+(x, y))
++(nil, ys) → ys
++(:(x, xs), ys) → :(x, ++(xs, ys))
sum(:(x, nil)) → :(x, nil)
sum(:(x, :(y, xs))) → sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) → sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(-(x, y), s(y)))
length(nil) → 0
length(:(x, xs)) → s(length(xs))
hd(:(x, xs)) → x
avg(xs) → quot(hd(sum(xs)), length(xs))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We deleted some edges using various graph approximations

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ EdgeDeletionProof
        ↳ QDP
          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

AVG(xs) → HD(sum(xs))
SUM(++(xs, :(x, :(y, ys)))) → ++1(xs, sum(:(x, :(y, ys))))
LENGTH(:(x, xs)) → LENGTH(xs)
QUOT(s(x), s(y)) → -1(x, y)
-1(s(x), s(y)) → -1(x, y)
+1(s(x), y) → +1(x, y)
AVG(xs) → QUOT(hd(sum(xs)), length(xs))
++1(:(x, xs), ys) → ++1(xs, ys)
AVG(xs) → SUM(xs)
SUM(:(x, :(y, xs))) → +1(x, y)
AVG(xs) → LENGTH(xs)
SUM(:(x, :(y, xs))) → SUM(:(+(x, y), xs))
QUOT(s(x), s(y)) → QUOT(-(x, y), s(y))
SUM(++(xs, :(x, :(y, ys)))) → SUM(:(x, :(y, ys)))
SUM(++(xs, :(x, :(y, ys)))) → SUM(++(xs, sum(:(x, :(y, ys)))))

The TRS R consists of the following rules:

+(0, y) → y
+(s(x), y) → s(+(x, y))
++(nil, ys) → ys
++(:(x, xs), ys) → :(x, ++(xs, ys))
sum(:(x, nil)) → :(x, nil)
sum(:(x, :(y, xs))) → sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) → sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(-(x, y), s(y)))
length(nil) → 0
length(:(x, xs)) → s(length(xs))
hd(:(x, xs)) → x
avg(xs) → quot(hd(sum(xs)), length(xs))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 7 SCCs with 8 less nodes.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ EdgeDeletionProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
                ↳ QDPOrderProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

LENGTH(:(x, xs)) → LENGTH(xs)

The TRS R consists of the following rules:

+(0, y) → y
+(s(x), y) → s(+(x, y))
++(nil, ys) → ys
++(:(x, xs), ys) → :(x, ++(xs, ys))
sum(:(x, nil)) → :(x, nil)
sum(:(x, :(y, xs))) → sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) → sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(-(x, y), s(y)))
length(nil) → 0
length(:(x, xs)) → s(length(xs))
hd(:(x, xs)) → x
avg(xs) → quot(hd(sum(xs)), length(xs))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


LENGTH(:(x, xs)) → LENGTH(xs)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
LENGTH(x1)  =  x1
:(x1, x2)  =  :(x1, x2)

Recursive path order with status [2].
Precedence:
trivial

Status:
:2: multiset

The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ EdgeDeletionProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
                ↳ QDPOrderProof
                  ↳ QDP
                    ↳ PisEmptyProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

+(0, y) → y
+(s(x), y) → s(+(x, y))
++(nil, ys) → ys
++(:(x, xs), ys) → :(x, ++(xs, ys))
sum(:(x, nil)) → :(x, nil)
sum(:(x, :(y, xs))) → sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) → sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(-(x, y), s(y)))
length(nil) → 0
length(:(x, xs)) → s(length(xs))
hd(:(x, xs)) → x
avg(xs) → quot(hd(sum(xs)), length(xs))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ EdgeDeletionProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ QDPOrderProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

-1(s(x), s(y)) → -1(x, y)

The TRS R consists of the following rules:

+(0, y) → y
+(s(x), y) → s(+(x, y))
++(nil, ys) → ys
++(:(x, xs), ys) → :(x, ++(xs, ys))
sum(:(x, nil)) → :(x, nil)
sum(:(x, :(y, xs))) → sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) → sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(-(x, y), s(y)))
length(nil) → 0
length(:(x, xs)) → s(length(xs))
hd(:(x, xs)) → x
avg(xs) → quot(hd(sum(xs)), length(xs))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


-1(s(x), s(y)) → -1(x, y)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
-1(x1, x2)  =  -1(x1)
s(x1)  =  s(x1)

Recursive path order with status [2].
Precedence:
s1 > -^11

Status:
-^11: multiset
s1: multiset

The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ EdgeDeletionProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ QDPOrderProof
                  ↳ QDP
                    ↳ PisEmptyProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

+(0, y) → y
+(s(x), y) → s(+(x, y))
++(nil, ys) → ys
++(:(x, xs), ys) → :(x, ++(xs, ys))
sum(:(x, nil)) → :(x, nil)
sum(:(x, :(y, xs))) → sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) → sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(-(x, y), s(y)))
length(nil) → 0
length(:(x, xs)) → s(length(xs))
hd(:(x, xs)) → x
avg(xs) → quot(hd(sum(xs)), length(xs))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ EdgeDeletionProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ QDPOrderProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

QUOT(s(x), s(y)) → QUOT(-(x, y), s(y))

The TRS R consists of the following rules:

+(0, y) → y
+(s(x), y) → s(+(x, y))
++(nil, ys) → ys
++(:(x, xs), ys) → :(x, ++(xs, ys))
sum(:(x, nil)) → :(x, nil)
sum(:(x, :(y, xs))) → sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) → sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(-(x, y), s(y)))
length(nil) → 0
length(:(x, xs)) → s(length(xs))
hd(:(x, xs)) → x
avg(xs) → quot(hd(sum(xs)), length(xs))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


QUOT(s(x), s(y)) → QUOT(-(x, y), s(y))
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
QUOT(x1, x2)  =  x1
s(x1)  =  s(x1)
-(x1, x2)  =  -(x1)
0  =  0

Recursive path order with status [2].
Precedence:
s1 > -1
0 > -1

Status:
-1: multiset
s1: multiset
0: multiset

The following usable rules [14] were oriented:

-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
-(x, 0) → x



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ EdgeDeletionProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ QDPOrderProof
                  ↳ QDP
                    ↳ PisEmptyProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

+(0, y) → y
+(s(x), y) → s(+(x, y))
++(nil, ys) → ys
++(:(x, xs), ys) → :(x, ++(xs, ys))
sum(:(x, nil)) → :(x, nil)
sum(:(x, :(y, xs))) → sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) → sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(-(x, y), s(y)))
length(nil) → 0
length(:(x, xs)) → s(length(xs))
hd(:(x, xs)) → x
avg(xs) → quot(hd(sum(xs)), length(xs))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ EdgeDeletionProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ QDPOrderProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

++1(:(x, xs), ys) → ++1(xs, ys)

The TRS R consists of the following rules:

+(0, y) → y
+(s(x), y) → s(+(x, y))
++(nil, ys) → ys
++(:(x, xs), ys) → :(x, ++(xs, ys))
sum(:(x, nil)) → :(x, nil)
sum(:(x, :(y, xs))) → sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) → sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(-(x, y), s(y)))
length(nil) → 0
length(:(x, xs)) → s(length(xs))
hd(:(x, xs)) → x
avg(xs) → quot(hd(sum(xs)), length(xs))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


++1(:(x, xs), ys) → ++1(xs, ys)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
++1(x1, x2)  =  ++1(x1)
:(x1, x2)  =  :(x1, x2)

Recursive path order with status [2].
Precedence:
:2 > ++^11

Status:
++^11: multiset
:2: multiset

The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ EdgeDeletionProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ QDPOrderProof
                  ↳ QDP
                    ↳ PisEmptyProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

+(0, y) → y
+(s(x), y) → s(+(x, y))
++(nil, ys) → ys
++(:(x, xs), ys) → :(x, ++(xs, ys))
sum(:(x, nil)) → :(x, nil)
sum(:(x, :(y, xs))) → sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) → sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(-(x, y), s(y)))
length(nil) → 0
length(:(x, xs)) → s(length(xs))
hd(:(x, xs)) → x
avg(xs) → quot(hd(sum(xs)), length(xs))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ EdgeDeletionProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ QDPOrderProof
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

+1(s(x), y) → +1(x, y)

The TRS R consists of the following rules:

+(0, y) → y
+(s(x), y) → s(+(x, y))
++(nil, ys) → ys
++(:(x, xs), ys) → :(x, ++(xs, ys))
sum(:(x, nil)) → :(x, nil)
sum(:(x, :(y, xs))) → sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) → sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(-(x, y), s(y)))
length(nil) → 0
length(:(x, xs)) → s(length(xs))
hd(:(x, xs)) → x
avg(xs) → quot(hd(sum(xs)), length(xs))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


+1(s(x), y) → +1(x, y)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
+1(x1, x2)  =  +1(x1)
s(x1)  =  s(x1)

Recursive path order with status [2].
Precedence:
s1 > +^11

Status:
+^11: multiset
s1: multiset

The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ EdgeDeletionProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ QDPOrderProof
                  ↳ QDP
                    ↳ PisEmptyProof
              ↳ QDP
              ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

+(0, y) → y
+(s(x), y) → s(+(x, y))
++(nil, ys) → ys
++(:(x, xs), ys) → :(x, ++(xs, ys))
sum(:(x, nil)) → :(x, nil)
sum(:(x, :(y, xs))) → sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) → sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(-(x, y), s(y)))
length(nil) → 0
length(:(x, xs)) → s(length(xs))
hd(:(x, xs)) → x
avg(xs) → quot(hd(sum(xs)), length(xs))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ EdgeDeletionProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ QDPOrderProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

SUM(:(x, :(y, xs))) → SUM(:(+(x, y), xs))

The TRS R consists of the following rules:

+(0, y) → y
+(s(x), y) → s(+(x, y))
++(nil, ys) → ys
++(:(x, xs), ys) → :(x, ++(xs, ys))
sum(:(x, nil)) → :(x, nil)
sum(:(x, :(y, xs))) → sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) → sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(-(x, y), s(y)))
length(nil) → 0
length(:(x, xs)) → s(length(xs))
hd(:(x, xs)) → x
avg(xs) → quot(hd(sum(xs)), length(xs))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


SUM(:(x, :(y, xs))) → SUM(:(+(x, y), xs))
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
SUM(x1)  =  SUM(x1)
:(x1, x2)  =  :(x1, x2)
+(x1, x2)  =  x2
0  =  0
s(x1)  =  s

Recursive path order with status [2].
Precedence:
:2 > SUM1 > s
0 > s

Status:
SUM1: multiset
0: multiset
s: multiset
:2: multiset

The following usable rules [14] were oriented:

+(0, y) → y
+(s(x), y) → s(+(x, y))



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ EdgeDeletionProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ QDPOrderProof
                  ↳ QDP
                    ↳ PisEmptyProof
              ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

+(0, y) → y
+(s(x), y) → s(+(x, y))
++(nil, ys) → ys
++(:(x, xs), ys) → :(x, ++(xs, ys))
sum(:(x, nil)) → :(x, nil)
sum(:(x, :(y, xs))) → sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) → sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(-(x, y), s(y)))
length(nil) → 0
length(:(x, xs)) → s(length(xs))
hd(:(x, xs)) → x
avg(xs) → quot(hd(sum(xs)), length(xs))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ EdgeDeletionProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

SUM(++(xs, :(x, :(y, ys)))) → SUM(++(xs, sum(:(x, :(y, ys)))))

The TRS R consists of the following rules:

+(0, y) → y
+(s(x), y) → s(+(x, y))
++(nil, ys) → ys
++(:(x, xs), ys) → :(x, ++(xs, ys))
sum(:(x, nil)) → :(x, nil)
sum(:(x, :(y, xs))) → sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) → sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(-(x, y), s(y)))
length(nil) → 0
length(:(x, xs)) → s(length(xs))
hd(:(x, xs)) → x
avg(xs) → quot(hd(sum(xs)), length(xs))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.